H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.308 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule List

((intersect :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

intersect :: Eq a => [a] -> [a] -> [a]

intersect

intersectBy (==)

intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

intersectBy

eq xs ys

concatMap (\vv2 ->

case	vv2 of
	x	->	if any (eq x) ys then x : [] else []
	_	->	[]

) xs

module Maybe where

import qualified List
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\vv2→

case vv2 of
x → if any (eq x) ys then x : [] else []

_ → []

is transformed to

intersectBy0 eq ys vv2 =

case vv2 of
x → if any (eq x) ys then x : [] else []

_ → []

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

mainModule List

((intersect :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

intersect :: Eq a => [a] -> [a] -> [a]

intersect

intersectBy (==)

intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

intersectBy

eq xs ys

concatMap (intersectBy0 eq ys) xs

intersectBy0

eq ys vv2

case	vv2 of
	x	->	if any (eq x) ys then x : [] else []
	_	->	[]

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case vv2 of
x → if any (eq x) ys then x : [] else []

_ → []

is transformed to

intersectBy00 eq ys x = if any (eq x) ys then x : [] else []

intersectBy00 eq ys _ = []

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

mainModule List

((intersect :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

intersect :: Eq a => [a] -> [a] -> [a]

intersect

intersectBy (==)

intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

intersectBy

eq xs ys

concatMap (intersectBy0 eq ys) xs

intersectBy0

eq ys vv2

intersectBy00 eq ys vv2

intersectBy00	eq ys x	=	if any (eq x) ys then x : [] else []
intersectBy00	eq ys _	=	[]

module Maybe where

import qualified List
import qualified Prelude

If Reductions:
The following If expression

if any (eq x) ys then x : [] else []

is transformed to

intersectBy000 x True = x : []

intersectBy000 x False = []

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

mainModule List

((intersect :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

intersect :: Eq a => [a] -> [a] -> [a]

intersect

intersectBy (==)

intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

intersectBy

eq xs ys

concatMap (intersectBy0 eq ys) xs

intersectBy0

eq ys vv2

intersectBy00 eq ys vv2

intersectBy00	eq ys x	=	intersectBy000 x (any (eq x) ys)
intersectBy00	eq ys _	=	[]

intersectBy000	x True	=	x : []
intersectBy000	x False	=	[]

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

mainModule List

((intersect :: [Int] -> [Int] -> [Int]) :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

intersect :: Eq a => [a] -> [a] -> [a]

intersect

intersectBy (==)

intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

intersectBy

eq xs ys

concatMap (intersectBy0 eq ys) xs

intersectBy0

eq ys vv2

intersectBy00 eq ys vv2

intersectBy00	eq ys x	=	intersectBy000 x (any (eq x) ys)
intersectBy00	eq ys vw	=	[]

intersectBy000	x True	=	x : []
intersectBy000	x False	=	[]

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ Narrow

mainModule List

(intersect :: [Int] -> [Int] -> [Int])

module List where

import qualified Maybe
import qualified Prelude

intersect :: Eq a => [a] -> [a] -> [a]

intersect

intersectBy (==)

intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

intersectBy

eq xs ys

concatMap (intersectBy0 eq ys) xs

intersectBy0

eq ys vv2

intersectBy00 eq ys vv2

intersectBy00	eq ys x	=	intersectBy000 x (any (eq x) ys)
intersectBy00	eq ys vw	=	[]

intersectBy000	x True	=	x : []
intersectBy000	x False	=	[]

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="intersect",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="intersect wv3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="intersect wv3 wv4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="intersectBy (==) wv3 wv4",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="concatMap (intersectBy0 (==) wv4) wv3",fontsize=16,color="black",shape="box"];6 -> 7[label="",style="solid", color="black", weight=3];
7[label="concat . map (intersectBy0 (==) wv4)",fontsize=16,color="black",shape="box"];7 -> 8[label="",style="solid", color="black", weight=3];
8[label="concat (map (intersectBy0 (==) wv4) wv3)",fontsize=16,color="black",shape="box"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="foldr (++) [] (map (intersectBy0 (==) wv4) wv3)",fontsize=16,color="burlywood",shape="triangle"];526[label="wv3/wv30 : wv31",fontsize=10,color="white",style="solid",shape="box"];9 -> 526[label="",style="solid", color="burlywood", weight=9];
526 -> 10[label="",style="solid", color="burlywood", weight=3];
527[label="wv3/[]",fontsize=10,color="white",style="solid",shape="box"];9 -> 527[label="",style="solid", color="burlywood", weight=9];
527 -> 11[label="",style="solid", color="burlywood", weight=3];
10[label="foldr (++) [] (map (intersectBy0 (==) wv4) (wv30 : wv31))",fontsize=16,color="black",shape="box"];10 -> 12[label="",style="solid", color="black", weight=3];
11[label="foldr (++) [] (map (intersectBy0 (==) wv4) [])",fontsize=16,color="black",shape="box"];11 -> 13[label="",style="solid", color="black", weight=3];
12[label="foldr (++) [] (intersectBy0 (==) wv4 wv30 : map (intersectBy0 (==) wv4) wv31)",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="foldr (++) [] []",fontsize=16,color="black",shape="box"];13 -> 15[label="",style="solid", color="black", weight=3];
14 -> 16[label="",style="dashed", color="red", weight=0];
14[label="(++) intersectBy0 (==) wv4 wv30 foldr (++) [] (map (intersectBy0 (==) wv4) wv31)",fontsize=16,color="magenta"];14 -> 17[label="",style="dashed", color="magenta", weight=3];
15[label="[]",fontsize=16,color="green",shape="box"];17 -> 9[label="",style="dashed", color="red", weight=0];
17[label="foldr (++) [] (map (intersectBy0 (==) wv4) wv31)",fontsize=16,color="magenta"];17 -> 18[label="",style="dashed", color="magenta", weight=3];
16[label="(++) intersectBy0 (==) wv4 wv30 wv5",fontsize=16,color="black",shape="triangle"];16 -> 19[label="",style="solid", color="black", weight=3];
18[label="wv31",fontsize=16,color="green",shape="box"];19[label="(++) intersectBy00 (==) wv4 wv30 wv5",fontsize=16,color="black",shape="box"];19 -> 20[label="",style="solid", color="black", weight=3];
20[label="(++) intersectBy000 wv30 (any ((==) wv30) wv4) wv5",fontsize=16,color="black",shape="box"];20 -> 21[label="",style="solid", color="black", weight=3];
21[label="(++) intersectBy000 wv30 (or . map ((==) wv30)) wv5",fontsize=16,color="black",shape="box"];21 -> 22[label="",style="solid", color="black", weight=3];
22[label="(++) intersectBy000 wv30 (or (map ((==) wv30) wv4)) wv5",fontsize=16,color="black",shape="box"];22 -> 23[label="",style="solid", color="black", weight=3];
23[label="(++) intersectBy000 wv30 (foldr (||) False (map ((==) wv30) wv4)) wv5",fontsize=16,color="burlywood",shape="box"];530[label="wv4/wv40 : wv41",fontsize=10,color="white",style="solid",shape="box"];23 -> 530[label="",style="solid", color="burlywood", weight=9];
530 -> 24[label="",style="solid", color="burlywood", weight=3];
531[label="wv4/[]",fontsize=10,color="white",style="solid",shape="box"];23 -> 531[label="",style="solid", color="burlywood", weight=9];
531 -> 25[label="",style="solid", color="burlywood", weight=3];
24[label="(++) intersectBy000 wv30 (foldr (||) False (map ((==) wv30) (wv40 : wv41))) wv5",fontsize=16,color="black",shape="box"];24 -> 26[label="",style="solid", color="black", weight=3];
25[label="(++) intersectBy000 wv30 (foldr (||) False (map ((==) wv30) [])) wv5",fontsize=16,color="black",shape="box"];25 -> 27[label="",style="solid", color="black", weight=3];
26[label="(++) intersectBy000 wv30 (foldr (||) False (((==) wv30 wv40) : map ((==) wv30) wv41)) wv5",fontsize=16,color="black",shape="box"];26 -> 28[label="",style="solid", color="black", weight=3];
27[label="(++) intersectBy000 wv30 (foldr (||) False []) wv5",fontsize=16,color="black",shape="triangle"];27 -> 29[label="",style="solid", color="black", weight=3];
28[label="(++) intersectBy000 wv30 ((||) (==) wv30 wv40 foldr (||) False (map ((==) wv30) wv41)) wv5",fontsize=16,color="black",shape="box"];28 -> 30[label="",style="solid", color="black", weight=3];
29[label="(++) intersectBy000 wv30 False wv5",fontsize=16,color="black",shape="box"];29 -> 31[label="",style="solid", color="black", weight=3];
30[label="(++) intersectBy000 wv30 ((||) primEqInt wv30 wv40 foldr (||) False (map (primEqInt wv30) wv41)) wv5",fontsize=16,color="burlywood",shape="triangle"];532[label="wv30/Pos wv300",fontsize=10,color="white",style="solid",shape="box"];30 -> 532[label="",style="solid", color="burlywood", weight=9];
532 -> 32[label="",style="solid", color="burlywood", weight=3];
533[label="wv30/Neg wv300",fontsize=10,color="white",style="solid",shape="box"];30 -> 533[label="",style="solid", color="burlywood", weight=9];
533 -> 33[label="",style="solid", color="burlywood", weight=3];
31[label="(++) [] wv5",fontsize=16,color="black",shape="triangle"];31 -> 34[label="",style="solid", color="black", weight=3];
32[label="(++) intersectBy000 (Pos wv300) ((||) primEqInt (Pos wv300) wv40 foldr (||) False (map (primEqInt (Pos wv300)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];534[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];32 -> 534[label="",style="solid", color="burlywood", weight=9];
534 -> 35[label="",style="solid", color="burlywood", weight=3];
535[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];32 -> 535[label="",style="solid", color="burlywood", weight=9];
535 -> 36[label="",style="solid", color="burlywood", weight=3];
33[label="(++) intersectBy000 (Neg wv300) ((||) primEqInt (Neg wv300) wv40 foldr (||) False (map (primEqInt (Neg wv300)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];536[label="wv300/Succ wv3000",fontsize=10,color="white",style="solid",shape="box"];33 -> 536[label="",style="solid", color="burlywood", weight=9];
536 -> 37[label="",style="solid", color="burlywood", weight=3];
537[label="wv300/Zero",fontsize=10,color="white",style="solid",shape="box"];33 -> 537[label="",style="solid", color="burlywood", weight=9];
537 -> 38[label="",style="solid", color="burlywood", weight=3];
34[label="wv5",fontsize=16,color="green",shape="box"];35[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) primEqInt (Pos (Succ wv3000)) wv40 foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];538[label="wv40/Pos wv400",fontsize=10,color="white",style="solid",shape="box"];35 -> 538[label="",style="solid", color="burlywood", weight=9];
538 -> 39[label="",style="solid", color="burlywood", weight=3];
539[label="wv40/Neg wv400",fontsize=10,color="white",style="solid",shape="box"];35 -> 539[label="",style="solid", color="burlywood", weight=9];
539 -> 40[label="",style="solid", color="burlywood", weight=3];
36[label="(++) intersectBy000 (Pos Zero) ((||) primEqInt (Pos Zero) wv40 foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];540[label="wv40/Pos wv400",fontsize=10,color="white",style="solid",shape="box"];36 -> 540[label="",style="solid", color="burlywood", weight=9];
540 -> 41[label="",style="solid", color="burlywood", weight=3];
541[label="wv40/Neg wv400",fontsize=10,color="white",style="solid",shape="box"];36 -> 541[label="",style="solid", color="burlywood", weight=9];
541 -> 42[label="",style="solid", color="burlywood", weight=3];
37[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) primEqInt (Neg (Succ wv3000)) wv40 foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];542[label="wv40/Pos wv400",fontsize=10,color="white",style="solid",shape="box"];37 -> 542[label="",style="solid", color="burlywood", weight=9];
542 -> 43[label="",style="solid", color="burlywood", weight=3];
543[label="wv40/Neg wv400",fontsize=10,color="white",style="solid",shape="box"];37 -> 543[label="",style="solid", color="burlywood", weight=9];
543 -> 44[label="",style="solid", color="burlywood", weight=3];
38[label="(++) intersectBy000 (Neg Zero) ((||) primEqInt (Neg Zero) wv40 foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];544[label="wv40/Pos wv400",fontsize=10,color="white",style="solid",shape="box"];38 -> 544[label="",style="solid", color="burlywood", weight=9];
544 -> 45[label="",style="solid", color="burlywood", weight=3];
545[label="wv40/Neg wv400",fontsize=10,color="white",style="solid",shape="box"];38 -> 545[label="",style="solid", color="burlywood", weight=9];
545 -> 46[label="",style="solid", color="burlywood", weight=3];
39[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) primEqInt (Pos (Succ wv3000)) (Pos wv400) foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];546[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];39 -> 546[label="",style="solid", color="burlywood", weight=9];
546 -> 47[label="",style="solid", color="burlywood", weight=3];
547[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];39 -> 547[label="",style="solid", color="burlywood", weight=9];
547 -> 48[label="",style="solid", color="burlywood", weight=3];
40[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) primEqInt (Pos (Succ wv3000)) (Neg wv400) foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="black",shape="box"];40 -> 49[label="",style="solid", color="black", weight=3];
41[label="(++) intersectBy000 (Pos Zero) ((||) primEqInt (Pos Zero) (Pos wv400) foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];548[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];41 -> 548[label="",style="solid", color="burlywood", weight=9];
548 -> 50[label="",style="solid", color="burlywood", weight=3];
549[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];41 -> 549[label="",style="solid", color="burlywood", weight=9];
549 -> 51[label="",style="solid", color="burlywood", weight=3];
42[label="(++) intersectBy000 (Pos Zero) ((||) primEqInt (Pos Zero) (Neg wv400) foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];550[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];42 -> 550[label="",style="solid", color="burlywood", weight=9];
550 -> 52[label="",style="solid", color="burlywood", weight=3];
551[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];42 -> 551[label="",style="solid", color="burlywood", weight=9];
551 -> 53[label="",style="solid", color="burlywood", weight=3];
43[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) primEqInt (Neg (Succ wv3000)) (Pos wv400) foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="black",shape="box"];43 -> 54[label="",style="solid", color="black", weight=3];
44[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) primEqInt (Neg (Succ wv3000)) (Neg wv400) foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];552[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];44 -> 552[label="",style="solid", color="burlywood", weight=9];
552 -> 55[label="",style="solid", color="burlywood", weight=3];
553[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];44 -> 553[label="",style="solid", color="burlywood", weight=9];
553 -> 56[label="",style="solid", color="burlywood", weight=3];
45[label="(++) intersectBy000 (Neg Zero) ((||) primEqInt (Neg Zero) (Pos wv400) foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];554[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];45 -> 554[label="",style="solid", color="burlywood", weight=9];
554 -> 57[label="",style="solid", color="burlywood", weight=3];
555[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];45 -> 555[label="",style="solid", color="burlywood", weight=9];
555 -> 58[label="",style="solid", color="burlywood", weight=3];
46[label="(++) intersectBy000 (Neg Zero) ((||) primEqInt (Neg Zero) (Neg wv400) foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];556[label="wv400/Succ wv4000",fontsize=10,color="white",style="solid",shape="box"];46 -> 556[label="",style="solid", color="burlywood", weight=9];
556 -> 59[label="",style="solid", color="burlywood", weight=3];
557[label="wv400/Zero",fontsize=10,color="white",style="solid",shape="box"];46 -> 557[label="",style="solid", color="burlywood", weight=9];
557 -> 60[label="",style="solid", color="burlywood", weight=3];
47[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) primEqInt (Pos (Succ wv3000)) (Pos (Succ wv4000)) foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="black",shape="box"];47 -> 61[label="",style="solid", color="black", weight=3];
48[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) primEqInt (Pos (Succ wv3000)) (Pos Zero) foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="black",shape="box"];48 -> 62[label="",style="solid", color="black", weight=3];
49[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) False foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="black",shape="triangle"];49 -> 63[label="",style="solid", color="black", weight=3];
50[label="(++) intersectBy000 (Pos Zero) ((||) primEqInt (Pos Zero) (Pos (Succ wv4000)) foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="black",shape="box"];50 -> 64[label="",style="solid", color="black", weight=3];
51[label="(++) intersectBy000 (Pos Zero) ((||) primEqInt (Pos Zero) (Pos Zero) foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="black",shape="box"];51 -> 65[label="",style="solid", color="black", weight=3];
52[label="(++) intersectBy000 (Pos Zero) ((||) primEqInt (Pos Zero) (Neg (Succ wv4000)) foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="black",shape="box"];52 -> 66[label="",style="solid", color="black", weight=3];
53[label="(++) intersectBy000 (Pos Zero) ((||) primEqInt (Pos Zero) (Neg Zero) foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="black",shape="box"];53 -> 67[label="",style="solid", color="black", weight=3];
54[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) False foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="black",shape="triangle"];54 -> 68[label="",style="solid", color="black", weight=3];
55[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) primEqInt (Neg (Succ wv3000)) (Neg (Succ wv4000)) foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="black",shape="box"];55 -> 69[label="",style="solid", color="black", weight=3];
56[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) primEqInt (Neg (Succ wv3000)) (Neg Zero) foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="black",shape="box"];56 -> 70[label="",style="solid", color="black", weight=3];
57[label="(++) intersectBy000 (Neg Zero) ((||) primEqInt (Neg Zero) (Pos (Succ wv4000)) foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="black",shape="box"];57 -> 71[label="",style="solid", color="black", weight=3];
58[label="(++) intersectBy000 (Neg Zero) ((||) primEqInt (Neg Zero) (Pos Zero) foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="black",shape="box"];58 -> 72[label="",style="solid", color="black", weight=3];
59[label="(++) intersectBy000 (Neg Zero) ((||) primEqInt (Neg Zero) (Neg (Succ wv4000)) foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="black",shape="box"];59 -> 73[label="",style="solid", color="black", weight=3];
60[label="(++) intersectBy000 (Neg Zero) ((||) primEqInt (Neg Zero) (Neg Zero) foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="black",shape="box"];60 -> 74[label="",style="solid", color="black", weight=3];
61 -> 388[label="",style="dashed", color="red", weight=0];
61[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) primEqNat wv3000 wv4000 foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="magenta"];61 -> 389[label="",style="dashed", color="magenta", weight=3];
61 -> 390[label="",style="dashed", color="magenta", weight=3];
61 -> 391[label="",style="dashed", color="magenta", weight=3];
61 -> 392[label="",style="dashed", color="magenta", weight=3];
61 -> 393[label="",style="dashed", color="magenta", weight=3];
62 -> 49[label="",style="dashed", color="red", weight=0];
62[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) False foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="magenta"];63[label="(++) intersectBy000 (Pos (Succ wv3000)) (foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];560[label="wv41/wv410 : wv411",fontsize=10,color="white",style="solid",shape="box"];63 -> 560[label="",style="solid", color="burlywood", weight=9];
560 -> 77[label="",style="solid", color="burlywood", weight=3];
561[label="wv41/[]",fontsize=10,color="white",style="solid",shape="box"];63 -> 561[label="",style="solid", color="burlywood", weight=9];
561 -> 78[label="",style="solid", color="burlywood", weight=3];
64[label="(++) intersectBy000 (Pos Zero) ((||) False foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="black",shape="triangle"];64 -> 79[label="",style="solid", color="black", weight=3];
65[label="(++) intersectBy000 (Pos Zero) ((||) True foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="black",shape="triangle"];65 -> 80[label="",style="solid", color="black", weight=3];
66 -> 64[label="",style="dashed", color="red", weight=0];
66[label="(++) intersectBy000 (Pos Zero) ((||) False foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="magenta"];67 -> 65[label="",style="dashed", color="red", weight=0];
67[label="(++) intersectBy000 (Pos Zero) ((||) True foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="magenta"];68[label="(++) intersectBy000 (Neg (Succ wv3000)) (foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];564[label="wv41/wv410 : wv411",fontsize=10,color="white",style="solid",shape="box"];68 -> 564[label="",style="solid", color="burlywood", weight=9];
564 -> 81[label="",style="solid", color="burlywood", weight=3];
565[label="wv41/[]",fontsize=10,color="white",style="solid",shape="box"];68 -> 565[label="",style="solid", color="burlywood", weight=9];
565 -> 82[label="",style="solid", color="burlywood", weight=3];
69 -> 436[label="",style="dashed", color="red", weight=0];
69[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) primEqNat wv3000 wv4000 foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="magenta"];69 -> 437[label="",style="dashed", color="magenta", weight=3];
69 -> 438[label="",style="dashed", color="magenta", weight=3];
69 -> 439[label="",style="dashed", color="magenta", weight=3];
69 -> 440[label="",style="dashed", color="magenta", weight=3];
69 -> 441[label="",style="dashed", color="magenta", weight=3];
70 -> 54[label="",style="dashed", color="red", weight=0];
70[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) False foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv41)) wv5",fontsize=16,color="magenta"];71[label="(++) intersectBy000 (Neg Zero) ((||) False foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="black",shape="triangle"];71 -> 85[label="",style="solid", color="black", weight=3];
72[label="(++) intersectBy000 (Neg Zero) ((||) True foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="black",shape="triangle"];72 -> 86[label="",style="solid", color="black", weight=3];
73 -> 71[label="",style="dashed", color="red", weight=0];
73[label="(++) intersectBy000 (Neg Zero) ((||) False foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="magenta"];74 -> 72[label="",style="dashed", color="red", weight=0];
74[label="(++) intersectBy000 (Neg Zero) ((||) True foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="magenta"];389[label="wv5",fontsize=16,color="green",shape="box"];390[label="wv41",fontsize=16,color="green",shape="box"];391[label="wv3000",fontsize=16,color="green",shape="box"];392[label="wv4000",fontsize=16,color="green",shape="box"];393[label="wv3000",fontsize=16,color="green",shape="box"];388[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) primEqNat wv14 wv15 foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="burlywood",shape="triangle"];570[label="wv14/Succ wv140",fontsize=10,color="white",style="solid",shape="box"];388 -> 570[label="",style="solid", color="burlywood", weight=9];
570 -> 434[label="",style="solid", color="burlywood", weight=3];
571[label="wv14/Zero",fontsize=10,color="white",style="solid",shape="box"];388 -> 571[label="",style="solid", color="burlywood", weight=9];
571 -> 435[label="",style="solid", color="burlywood", weight=3];
77[label="(++) intersectBy000 (Pos (Succ wv3000)) (foldr (||) False (map (primEqInt (Pos (Succ wv3000))) (wv410 : wv411))) wv5",fontsize=16,color="black",shape="box"];77 -> 91[label="",style="solid", color="black", weight=3];
78[label="(++) intersectBy000 (Pos (Succ wv3000)) (foldr (||) False (map (primEqInt (Pos (Succ wv3000))) [])) wv5",fontsize=16,color="black",shape="box"];78 -> 92[label="",style="solid", color="black", weight=3];
79[label="(++) intersectBy000 (Pos Zero) (foldr (||) False (map (primEqInt (Pos Zero)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];572[label="wv41/wv410 : wv411",fontsize=10,color="white",style="solid",shape="box"];79 -> 572[label="",style="solid", color="burlywood", weight=9];
572 -> 93[label="",style="solid", color="burlywood", weight=3];
573[label="wv41/[]",fontsize=10,color="white",style="solid",shape="box"];79 -> 573[label="",style="solid", color="burlywood", weight=9];
573 -> 94[label="",style="solid", color="burlywood", weight=3];
80[label="(++) intersectBy000 (Pos Zero) True wv5",fontsize=16,color="black",shape="box"];80 -> 95[label="",style="solid", color="black", weight=3];
81[label="(++) intersectBy000 (Neg (Succ wv3000)) (foldr (||) False (map (primEqInt (Neg (Succ wv3000))) (wv410 : wv411))) wv5",fontsize=16,color="black",shape="box"];81 -> 96[label="",style="solid", color="black", weight=3];
82[label="(++) intersectBy000 (Neg (Succ wv3000)) (foldr (||) False (map (primEqInt (Neg (Succ wv3000))) [])) wv5",fontsize=16,color="black",shape="box"];82 -> 97[label="",style="solid", color="black", weight=3];
437[label="wv4000",fontsize=16,color="green",shape="box"];438[label="wv3000",fontsize=16,color="green",shape="box"];439[label="wv41",fontsize=16,color="green",shape="box"];440[label="wv5",fontsize=16,color="green",shape="box"];441[label="wv3000",fontsize=16,color="green",shape="box"];436[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) primEqNat wv20 wv21 foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="burlywood",shape="triangle"];574[label="wv20/Succ wv200",fontsize=10,color="white",style="solid",shape="box"];436 -> 574[label="",style="solid", color="burlywood", weight=9];
574 -> 482[label="",style="solid", color="burlywood", weight=3];
575[label="wv20/Zero",fontsize=10,color="white",style="solid",shape="box"];436 -> 575[label="",style="solid", color="burlywood", weight=9];
575 -> 483[label="",style="solid", color="burlywood", weight=3];
85[label="(++) intersectBy000 (Neg Zero) (foldr (||) False (map (primEqInt (Neg Zero)) wv41)) wv5",fontsize=16,color="burlywood",shape="box"];576[label="wv41/wv410 : wv411",fontsize=10,color="white",style="solid",shape="box"];85 -> 576[label="",style="solid", color="burlywood", weight=9];
576 -> 102[label="",style="solid", color="burlywood", weight=3];
577[label="wv41/[]",fontsize=10,color="white",style="solid",shape="box"];85 -> 577[label="",style="solid", color="burlywood", weight=9];
577 -> 103[label="",style="solid", color="burlywood", weight=3];
86[label="(++) intersectBy000 (Neg Zero) True wv5",fontsize=16,color="black",shape="box"];86 -> 104[label="",style="solid", color="black", weight=3];
434[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) primEqNat (Succ wv140) wv15 foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="burlywood",shape="box"];578[label="wv15/Succ wv150",fontsize=10,color="white",style="solid",shape="box"];434 -> 578[label="",style="solid", color="burlywood", weight=9];
578 -> 484[label="",style="solid", color="burlywood", weight=3];
579[label="wv15/Zero",fontsize=10,color="white",style="solid",shape="box"];434 -> 579[label="",style="solid", color="burlywood", weight=9];
579 -> 485[label="",style="solid", color="burlywood", weight=3];
435[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) primEqNat Zero wv15 foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="burlywood",shape="box"];580[label="wv15/Succ wv150",fontsize=10,color="white",style="solid",shape="box"];435 -> 580[label="",style="solid", color="burlywood", weight=9];
580 -> 486[label="",style="solid", color="burlywood", weight=3];
581[label="wv15/Zero",fontsize=10,color="white",style="solid",shape="box"];435 -> 581[label="",style="solid", color="burlywood", weight=9];
581 -> 487[label="",style="solid", color="burlywood", weight=3];
91[label="(++) intersectBy000 (Pos (Succ wv3000)) (foldr (||) False (primEqInt (Pos (Succ wv3000)) wv410 : map (primEqInt (Pos (Succ wv3000))) wv411)) wv5",fontsize=16,color="black",shape="box"];91 -> 109[label="",style="solid", color="black", weight=3];
92 -> 27[label="",style="dashed", color="red", weight=0];
92[label="(++) intersectBy000 (Pos (Succ wv3000)) (foldr (||) False []) wv5",fontsize=16,color="magenta"];92 -> 110[label="",style="dashed", color="magenta", weight=3];
93[label="(++) intersectBy000 (Pos Zero) (foldr (||) False (map (primEqInt (Pos Zero)) (wv410 : wv411))) wv5",fontsize=16,color="black",shape="box"];93 -> 111[label="",style="solid", color="black", weight=3];
94[label="(++) intersectBy000 (Pos Zero) (foldr (||) False (map (primEqInt (Pos Zero)) [])) wv5",fontsize=16,color="black",shape="box"];94 -> 112[label="",style="solid", color="black", weight=3];
95[label="(++) (Pos Zero : []) wv5",fontsize=16,color="black",shape="box"];95 -> 113[label="",style="solid", color="black", weight=3];
96[label="(++) intersectBy000 (Neg (Succ wv3000)) (foldr (||) False (primEqInt (Neg (Succ wv3000)) wv410 : map (primEqInt (Neg (Succ wv3000))) wv411)) wv5",fontsize=16,color="black",shape="box"];96 -> 114[label="",style="solid", color="black", weight=3];
97 -> 27[label="",style="dashed", color="red", weight=0];
97[label="(++) intersectBy000 (Neg (Succ wv3000)) (foldr (||) False []) wv5",fontsize=16,color="magenta"];97 -> 115[label="",style="dashed", color="magenta", weight=3];
482[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) primEqNat (Succ wv200) wv21 foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="burlywood",shape="box"];584[label="wv21/Succ wv210",fontsize=10,color="white",style="solid",shape="box"];482 -> 584[label="",style="solid", color="burlywood", weight=9];
584 -> 488[label="",style="solid", color="burlywood", weight=3];
585[label="wv21/Zero",fontsize=10,color="white",style="solid",shape="box"];482 -> 585[label="",style="solid", color="burlywood", weight=9];
585 -> 489[label="",style="solid", color="burlywood", weight=3];
483[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) primEqNat Zero wv21 foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="burlywood",shape="box"];586[label="wv21/Succ wv210",fontsize=10,color="white",style="solid",shape="box"];483 -> 586[label="",style="solid", color="burlywood", weight=9];
586 -> 490[label="",style="solid", color="burlywood", weight=3];
587[label="wv21/Zero",fontsize=10,color="white",style="solid",shape="box"];483 -> 587[label="",style="solid", color="burlywood", weight=9];
587 -> 491[label="",style="solid", color="burlywood", weight=3];
102[label="(++) intersectBy000 (Neg Zero) (foldr (||) False (map (primEqInt (Neg Zero)) (wv410 : wv411))) wv5",fontsize=16,color="black",shape="box"];102 -> 120[label="",style="solid", color="black", weight=3];
103[label="(++) intersectBy000 (Neg Zero) (foldr (||) False (map (primEqInt (Neg Zero)) [])) wv5",fontsize=16,color="black",shape="box"];103 -> 121[label="",style="solid", color="black", weight=3];
104[label="(++) (Neg Zero : []) wv5",fontsize=16,color="black",shape="box"];104 -> 122[label="",style="solid", color="black", weight=3];
484[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) primEqNat (Succ wv140) (Succ wv150) foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="black",shape="box"];484 -> 492[label="",style="solid", color="black", weight=3];
485[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) primEqNat (Succ wv140) Zero foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="black",shape="box"];485 -> 493[label="",style="solid", color="black", weight=3];
486[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) primEqNat Zero (Succ wv150) foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="black",shape="box"];486 -> 494[label="",style="solid", color="black", weight=3];
487[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) primEqNat Zero Zero foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="black",shape="box"];487 -> 495[label="",style="solid", color="black", weight=3];
109 -> 30[label="",style="dashed", color="red", weight=0];
109[label="(++) intersectBy000 (Pos (Succ wv3000)) ((||) primEqInt (Pos (Succ wv3000)) wv410 foldr (||) False (map (primEqInt (Pos (Succ wv3000))) wv411)) wv5",fontsize=16,color="magenta"];109 -> 128[label="",style="dashed", color="magenta", weight=3];
109 -> 129[label="",style="dashed", color="magenta", weight=3];
109 -> 130[label="",style="dashed", color="magenta", weight=3];
110[label="Pos (Succ wv3000)",fontsize=16,color="green",shape="box"];111[label="(++) intersectBy000 (Pos Zero) (foldr (||) False (primEqInt (Pos Zero) wv410 : map (primEqInt (Pos Zero)) wv411)) wv5",fontsize=16,color="black",shape="box"];111 -> 131[label="",style="solid", color="black", weight=3];
112 -> 27[label="",style="dashed", color="red", weight=0];
112[label="(++) intersectBy000 (Pos Zero) (foldr (||) False []) wv5",fontsize=16,color="magenta"];112 -> 132[label="",style="dashed", color="magenta", weight=3];
113[label="Pos Zero : [] ++ wv5",fontsize=16,color="green",shape="box"];113 -> 133[label="",style="dashed", color="green", weight=3];
114 -> 30[label="",style="dashed", color="red", weight=0];
114[label="(++) intersectBy000 (Neg (Succ wv3000)) ((||) primEqInt (Neg (Succ wv3000)) wv410 foldr (||) False (map (primEqInt (Neg (Succ wv3000))) wv411)) wv5",fontsize=16,color="magenta"];114 -> 134[label="",style="dashed", color="magenta", weight=3];
114 -> 135[label="",style="dashed", color="magenta", weight=3];
114 -> 136[label="",style="dashed", color="magenta", weight=3];
115[label="Neg (Succ wv3000)",fontsize=16,color="green",shape="box"];488[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) primEqNat (Succ wv200) (Succ wv210) foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="black",shape="box"];488 -> 496[label="",style="solid", color="black", weight=3];
489[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) primEqNat (Succ wv200) Zero foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="black",shape="box"];489 -> 497[label="",style="solid", color="black", weight=3];
490[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) primEqNat Zero (Succ wv210) foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="black",shape="box"];490 -> 498[label="",style="solid", color="black", weight=3];
491[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) primEqNat Zero Zero foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="black",shape="box"];491 -> 499[label="",style="solid", color="black", weight=3];
120[label="(++) intersectBy000 (Neg Zero) (foldr (||) False (primEqInt (Neg Zero) wv410 : map (primEqInt (Neg Zero)) wv411)) wv5",fontsize=16,color="black",shape="box"];120 -> 142[label="",style="solid", color="black", weight=3];
121 -> 27[label="",style="dashed", color="red", weight=0];
121[label="(++) intersectBy000 (Neg Zero) (foldr (||) False []) wv5",fontsize=16,color="magenta"];121 -> 143[label="",style="dashed", color="magenta", weight=3];
122[label="Neg Zero : [] ++ wv5",fontsize=16,color="green",shape="box"];122 -> 144[label="",style="dashed", color="green", weight=3];
492 -> 388[label="",style="dashed", color="red", weight=0];
492[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) primEqNat wv140 wv150 foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="magenta"];492 -> 500[label="",style="dashed", color="magenta", weight=3];
492 -> 501[label="",style="dashed", color="magenta", weight=3];
493 -> 49[label="",style="dashed", color="red", weight=0];
493[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) False foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="magenta"];493 -> 502[label="",style="dashed", color="magenta", weight=3];
493 -> 503[label="",style="dashed", color="magenta", weight=3];
493 -> 504[label="",style="dashed", color="magenta", weight=3];
494 -> 49[label="",style="dashed", color="red", weight=0];
494[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) False foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="magenta"];494 -> 505[label="",style="dashed", color="magenta", weight=3];
494 -> 506[label="",style="dashed", color="magenta", weight=3];
494 -> 507[label="",style="dashed", color="magenta", weight=3];
495[label="(++) intersectBy000 (Pos (Succ wv13)) ((||) True foldr (||) False (map (primEqInt (Pos (Succ wv13))) wv16)) wv17",fontsize=16,color="black",shape="box"];495 -> 508[label="",style="solid", color="black", weight=3];
128[label="wv411",fontsize=16,color="green",shape="box"];129[label="Pos (Succ wv3000)",fontsize=16,color="green",shape="box"];130[label="wv410",fontsize=16,color="green",shape="box"];131 -> 30[label="",style="dashed", color="red", weight=0];
131[label="(++) intersectBy000 (Pos Zero) ((||) primEqInt (Pos Zero) wv410 foldr (||) False (map (primEqInt (Pos Zero)) wv411)) wv5",fontsize=16,color="magenta"];131 -> 150[label="",style="dashed", color="magenta", weight=3];
131 -> 151[label="",style="dashed", color="magenta", weight=3];
131 -> 152[label="",style="dashed", color="magenta", weight=3];
132[label="Pos Zero",fontsize=16,color="green",shape="box"];133 -> 31[label="",style="dashed", color="red", weight=0];
133[label="[] ++ wv5",fontsize=16,color="magenta"];134[label="wv411",fontsize=16,color="green",shape="box"];135[label="Neg (Succ wv3000)",fontsize=16,color="green",shape="box"];136[label="wv410",fontsize=16,color="green",shape="box"];496 -> 436[label="",style="dashed", color="red", weight=0];
496[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) primEqNat wv200 wv210 foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="magenta"];496 -> 509[label="",style="dashed", color="magenta", weight=3];
496 -> 510[label="",style="dashed", color="magenta", weight=3];
497 -> 54[label="",style="dashed", color="red", weight=0];
497[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) False foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="magenta"];497 -> 511[label="",style="dashed", color="magenta", weight=3];
497 -> 512[label="",style="dashed", color="magenta", weight=3];
497 -> 513[label="",style="dashed", color="magenta", weight=3];
498 -> 54[label="",style="dashed", color="red", weight=0];
498[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) False foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="magenta"];498 -> 514[label="",style="dashed", color="magenta", weight=3];
498 -> 515[label="",style="dashed", color="magenta", weight=3];
498 -> 516[label="",style="dashed", color="magenta", weight=3];
499[label="(++) intersectBy000 (Neg (Succ wv19)) ((||) True foldr (||) False (map (primEqInt (Neg (Succ wv19))) wv22)) wv23",fontsize=16,color="black",shape="box"];499 -> 517[label="",style="solid", color="black", weight=3];
142 -> 30[label="",style="dashed", color="red", weight=0];
142[label="(++) intersectBy000 (Neg Zero) ((||) primEqInt (Neg Zero) wv410 foldr (||) False (map (primEqInt (Neg Zero)) wv411)) wv5",fontsize=16,color="magenta"];142 -> 158[label="",style="dashed", color="magenta", weight=3];
142 -> 159[label="",style="dashed", color="magenta", weight=3];
142 -> 160[label="",style="dashed", color="magenta", weight=3];
143[label="Neg Zero",fontsize=16,color="green",shape="box"];144 -> 31[label="",style="dashed", color="red", weight=0];
144[label="[] ++ wv5",fontsize=16,color="magenta"];500[label="wv150",fontsize=16,color="green",shape="box"];501[label="wv140",fontsize=16,color="green",shape="box"];502[label="wv17",fontsize=16,color="green",shape="box"];503[label="wv16",fontsize=16,color="green",shape="box"];504[label="wv13",fontsize=16,color="green",shape="box"];505[label="wv17",fontsize=16,color="green",shape="box"];506[label="wv16",fontsize=16,color="green",shape="box"];507[label="wv13",fontsize=16,color="green",shape="box"];508[label="(++) intersectBy000 (Pos (Succ wv13)) True wv17",fontsize=16,color="black",shape="box"];508 -> 518[label="",style="solid", color="black", weight=3];
150[label="wv411",fontsize=16,color="green",shape="box"];151[label="Pos Zero",fontsize=16,color="green",shape="box"];152[label="wv410",fontsize=16,color="green",shape="box"];509[label="wv210",fontsize=16,color="green",shape="box"];510[label="wv200",fontsize=16,color="green",shape="box"];511[label="wv23",fontsize=16,color="green",shape="box"];512[label="wv22",fontsize=16,color="green",shape="box"];513[label="wv19",fontsize=16,color="green",shape="box"];514[label="wv23",fontsize=16,color="green",shape="box"];515[label="wv22",fontsize=16,color="green",shape="box"];516[label="wv19",fontsize=16,color="green",shape="box"];517[label="(++) intersectBy000 (Neg (Succ wv19)) True wv23",fontsize=16,color="black",shape="box"];517 -> 519[label="",style="solid", color="black", weight=3];
158[label="wv411",fontsize=16,color="green",shape="box"];159[label="Neg Zero",fontsize=16,color="green",shape="box"];160[label="wv410",fontsize=16,color="green",shape="box"];518[label="(++) (Pos (Succ wv13) : []) wv17",fontsize=16,color="black",shape="box"];518 -> 520[label="",style="solid", color="black", weight=3];
519[label="(++) (Neg (Succ wv19) : []) wv23",fontsize=16,color="black",shape="box"];519 -> 521[label="",style="solid", color="black", weight=3];
520[label="Pos (Succ wv13) : [] ++ wv17",fontsize=16,color="green",shape="box"];520 -> 522[label="",style="dashed", color="green", weight=3];
521[label="Neg (Succ wv19) : [] ++ wv23",fontsize=16,color="green",shape="box"];521 -> 523[label="",style="dashed", color="green", weight=3];
522 -> 31[label="",style="dashed", color="red", weight=0];
522[label="[] ++ wv17",fontsize=16,color="magenta"];522 -> 524[label="",style="dashed", color="magenta", weight=3];
523 -> 31[label="",style="dashed", color="red", weight=0];
523[label="[] ++ wv23",fontsize=16,color="magenta"];523 -> 525[label="",style="dashed", color="magenta", weight=3];
524[label="wv17",fontsize=16,color="green",shape="box"];525[label="wv23",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ DependencyGraphProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(Neg(Zero), Neg(Succ(wv4000)), wv41, wv5) → new_psPs5(wv41, wv5)
new_psPs1(Pos(Succ(wv3000)), Pos(Zero), wv41, wv5) → new_psPs0(wv3000, wv41, wv5)
new_psPs3(wv19, Succ(wv200), Succ(wv210), wv22, wv23) → new_psPs3(wv19, wv200, wv210, wv22, wv23)
new_psPs4(wv3000, :(wv410, wv411), wv5) → new_psPs1(Neg(Succ(wv3000)), wv410, wv411, wv5)
new_psPs5(:(wv410, wv411), wv5) → new_psPs1(Neg(Zero), wv410, wv411, wv5)
new_psPs1(Neg(Succ(wv3000)), Neg(Zero), wv41, wv5) → new_psPs4(wv3000, wv41, wv5)
new_psPs1(Pos(Zero), Neg(Succ(wv4000)), wv41, wv5) → new_psPs2(wv41, wv5)
new_psPs1(Pos(Succ(wv3000)), Pos(Succ(wv4000)), wv41, wv5) → new_psPs(wv3000, wv3000, wv4000, wv41, wv5)
new_psPs1(Neg(Succ(wv3000)), Neg(Succ(wv4000)), wv41, wv5) → new_psPs3(wv3000, wv3000, wv4000, wv41, wv5)
new_psPs2(:(wv410, wv411), wv5) → new_psPs1(Pos(Zero), wv410, wv411, wv5)
new_psPs(wv13, Succ(wv140), Zero, wv16, wv17) → new_psPs0(wv13, wv16, wv17)
new_psPs(wv13, Zero, Succ(wv150), wv16, wv17) → new_psPs0(wv13, wv16, wv17)
new_psPs1(Pos(Zero), Pos(Succ(wv4000)), :(wv410, wv411), wv5) → new_psPs1(Pos(Zero), wv410, wv411, wv5)
new_psPs1(Pos(Succ(wv3000)), Neg(wv400), :(wv410, wv411), wv5) → new_psPs1(Pos(Succ(wv3000)), wv410, wv411, wv5)
new_psPs(wv13, Succ(wv140), Succ(wv150), wv16, wv17) → new_psPs(wv13, wv140, wv150, wv16, wv17)
new_psPs1(Neg(Zero), Pos(Succ(wv4000)), :(wv410, wv411), wv5) → new_psPs1(Neg(Zero), wv410, wv411, wv5)
new_psPs1(Neg(Succ(wv3000)), Pos(wv400), :(wv410, wv411), wv5) → new_psPs1(Neg(Succ(wv3000)), wv410, wv411, wv5)
new_psPs0(wv3000, :(wv410, wv411), wv5) → new_psPs1(Pos(Succ(wv3000)), wv410, wv411, wv5)
new_psPs3(wv19, Succ(wv200), Zero, wv22, wv23) → new_psPs4(wv19, wv22, wv23)
new_psPs3(wv19, Zero, Succ(wv210), wv22, wv23) → new_psPs4(wv19, wv22, wv23)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ QDPSizeChangeProof

                                ↳ QDP

                                ↳ QDP

                                ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs2(:(wv410, wv411), wv5) → new_psPs1(Pos(Zero), wv410, wv411, wv5)
new_psPs1(Pos(Zero), Pos(Succ(wv4000)), :(wv410, wv411), wv5) → new_psPs1(Pos(Zero), wv410, wv411, wv5)
new_psPs1(Pos(Zero), Neg(Succ(wv4000)), wv41, wv5) → new_psPs2(wv41, wv5)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_psPs1(Pos(Zero), Neg(Succ(wv4000)), wv41, wv5) → new_psPs2(wv41, wv5)
The graph contains the following edges 3 >= 1, 4 >= 2
new_psPs1(Pos(Zero), Pos(Succ(wv4000)), :(wv410, wv411), wv5) → new_psPs1(Pos(Zero), wv410, wv411, wv5)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3, 4 >= 4
new_psPs2(:(wv410, wv411), wv5) → new_psPs1(Pos(Zero), wv410, wv411, wv5)
The graph contains the following edges 1 > 2, 1 > 3, 2 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ QDPSizeChangeProof

                                ↳ QDP

                                ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(Neg(Succ(wv3000)), Neg(Succ(wv4000)), wv41, wv5) → new_psPs3(wv3000, wv3000, wv4000, wv41, wv5)
new_psPs3(wv19, Succ(wv200), Succ(wv210), wv22, wv23) → new_psPs3(wv19, wv200, wv210, wv22, wv23)
new_psPs1(Neg(Succ(wv3000)), Pos(wv400), :(wv410, wv411), wv5) → new_psPs1(Neg(Succ(wv3000)), wv410, wv411, wv5)
new_psPs3(wv19, Succ(wv200), Zero, wv22, wv23) → new_psPs4(wv19, wv22, wv23)
new_psPs4(wv3000, :(wv410, wv411), wv5) → new_psPs1(Neg(Succ(wv3000)), wv410, wv411, wv5)
new_psPs3(wv19, Zero, Succ(wv210), wv22, wv23) → new_psPs4(wv19, wv22, wv23)
new_psPs1(Neg(Succ(wv3000)), Neg(Zero), wv41, wv5) → new_psPs4(wv3000, wv41, wv5)

From the DPs we obtained the following set of size-change graphs:

new_psPs4(wv3000, :(wv410, wv411), wv5) → new_psPs1(Neg(Succ(wv3000)), wv410, wv411, wv5)
The graph contains the following edges 2 > 2, 2 > 3, 3 >= 4
new_psPs1(Neg(Succ(wv3000)), Neg(Succ(wv4000)), wv41, wv5) → new_psPs3(wv3000, wv3000, wv4000, wv41, wv5)
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3, 3 >= 4, 4 >= 5
new_psPs3(wv19, Succ(wv200), Succ(wv210), wv22, wv23) → new_psPs3(wv19, wv200, wv210, wv22, wv23)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5
new_psPs1(Neg(Succ(wv3000)), Neg(Zero), wv41, wv5) → new_psPs4(wv3000, wv41, wv5)
The graph contains the following edges 1 > 1, 3 >= 2, 4 >= 3
new_psPs1(Neg(Succ(wv3000)), Pos(wv400), :(wv410, wv411), wv5) → new_psPs1(Neg(Succ(wv3000)), wv410, wv411, wv5)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3, 4 >= 4
new_psPs3(wv19, Zero, Succ(wv210), wv22, wv23) → new_psPs4(wv19, wv22, wv23)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3
new_psPs3(wv19, Succ(wv200), Zero, wv22, wv23) → new_psPs4(wv19, wv22, wv23)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                ↳ QDP

                                  ↳ QDPSizeChangeProof

                                ↳ QDP

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(Pos(Succ(wv3000)), Pos(Succ(wv4000)), wv41, wv5) → new_psPs(wv3000, wv3000, wv4000, wv41, wv5)
new_psPs(wv13, Zero, Succ(wv150), wv16, wv17) → new_psPs0(wv13, wv16, wv17)
new_psPs(wv13, Succ(wv140), Zero, wv16, wv17) → new_psPs0(wv13, wv16, wv17)
new_psPs1(Pos(Succ(wv3000)), Neg(wv400), :(wv410, wv411), wv5) → new_psPs1(Pos(Succ(wv3000)), wv410, wv411, wv5)
new_psPs1(Pos(Succ(wv3000)), Pos(Zero), wv41, wv5) → new_psPs0(wv3000, wv41, wv5)
new_psPs(wv13, Succ(wv140), Succ(wv150), wv16, wv17) → new_psPs(wv13, wv140, wv150, wv16, wv17)
new_psPs0(wv3000, :(wv410, wv411), wv5) → new_psPs1(Pos(Succ(wv3000)), wv410, wv411, wv5)

From the DPs we obtained the following set of size-change graphs:

new_psPs1(Pos(Succ(wv3000)), Pos(Zero), wv41, wv5) → new_psPs0(wv3000, wv41, wv5)
The graph contains the following edges 1 > 1, 3 >= 2, 4 >= 3
new_psPs1(Pos(Succ(wv3000)), Neg(wv400), :(wv410, wv411), wv5) → new_psPs1(Pos(Succ(wv3000)), wv410, wv411, wv5)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3, 4 >= 4
new_psPs1(Pos(Succ(wv3000)), Pos(Succ(wv4000)), wv41, wv5) → new_psPs(wv3000, wv3000, wv4000, wv41, wv5)
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3, 3 >= 4, 4 >= 5
new_psPs0(wv3000, :(wv410, wv411), wv5) → new_psPs1(Pos(Succ(wv3000)), wv410, wv411, wv5)
The graph contains the following edges 2 > 2, 2 > 3, 3 >= 4
new_psPs(wv13, Succ(wv140), Succ(wv150), wv16, wv17) → new_psPs(wv13, wv140, wv150, wv16, wv17)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4, 5 >= 5
new_psPs(wv13, Succ(wv140), Zero, wv16, wv17) → new_psPs0(wv13, wv16, wv17)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3
new_psPs(wv13, Zero, Succ(wv150), wv16, wv17) → new_psPs0(wv13, wv16, wv17)
The graph contains the following edges 1 >= 1, 4 >= 2, 5 >= 3

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                ↳ QDP

                                ↳ QDP

                                  ↳ QDPSizeChangeProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(Neg(Zero), Neg(Succ(wv4000)), wv41, wv5) → new_psPs5(wv41, wv5)
new_psPs1(Neg(Zero), Pos(Succ(wv4000)), :(wv410, wv411), wv5) → new_psPs1(Neg(Zero), wv410, wv411, wv5)
new_psPs5(:(wv410, wv411), wv5) → new_psPs1(Neg(Zero), wv410, wv411, wv5)

From the DPs we obtained the following set of size-change graphs:

new_psPs1(Neg(Zero), Neg(Succ(wv4000)), wv41, wv5) → new_psPs5(wv41, wv5)
The graph contains the following edges 3 >= 1, 4 >= 2
new_psPs1(Neg(Zero), Pos(Succ(wv4000)), :(wv410, wv411), wv5) → new_psPs1(Neg(Zero), wv410, wv411, wv5)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3, 4 >= 4
new_psPs5(:(wv410, wv411), wv5) → new_psPs1(Neg(Zero), wv410, wv411, wv5)
The graph contains the following edges 1 > 2, 1 > 3, 2 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ CR

        ↳ HASKELL

          ↳ IFR

            ↳ HASKELL

              ↳ BR

                ↳ HASKELL

                  ↳ COR

                    ↳ HASKELL

                      ↳ Narrow

                        ↳ AND

                          ↳ QDP

                          ↳ QDP

                            ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(wv4, :(wv30, wv31)) → new_foldr(wv4, wv31)

From the DPs we obtained the following set of size-change graphs:

new_foldr(wv4, :(wv30, wv31)) → new_foldr(wv4, wv31)
The graph contains the following edges 1 >= 1, 2 > 2

intersectBy00	eq ys x	= if any (eq x) ys then x : [] else []
intersectBy00	eq ys _	= []